/* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files
 * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify,
 * merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF
 * OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 */

package edu.mit.csail.sdg.alloy4compiler.ast;

import java.util.ArrayList;
import java.util.Collection;
import java.util.List;
import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorType;
import edu.mit.csail.sdg.alloy4.ErrorWarning;
import edu.mit.csail.sdg.alloy4.ConstList;
import static edu.mit.csail.sdg.alloy4compiler.ast.Sig.SIGINT;
import static edu.mit.csail.sdg.alloy4compiler.ast.Type.EMPTY;

/** Immutable; represents an unresolved node that has several possibilities. */

public final class ExprChoice extends Expr {

    /** The unmodifiable list of Expr(s) from that this ExprChoice can refer to. */
    public final ConstList<Expr> choices;

    /** The unmodifiable list of String(s) explaining where each choice came from. */
    public final ConstList<String> reasons;

    /** Caches the span() result. */
    private Pos span=null;

    //============================================================================================================//

    /** {@inheritDoc} */
    @Override public Pos span() {
        Pos p=span;
        if (p==null) {
            p=pos;
            for(Expr a:choices) p=p.merge(a.span());
            span=p;
        }
        return p;
    }

    //============================================================================================================//

    /** {@inheritDoc} */
    @Override public void toString(StringBuilder out, int indent) {
        if (indent<0) {
            out.append("<");
            for(Expr e:choices) { e.toString(out,-1); out.append(";"); }
            out.append(">");
        } else {
            for(int i=0; i<indent; i++) { out.append(' '); }
            out.append(""+choices.size()+" choices with combined type=").append(type).append('\n');
        }
    }

    //============================================================================================================//

    /** Generate an appropriate error message in the case where there are no legal choices. */
    private static Err complain(Pos pos, ConstList<Expr> choices) {
        StringBuilder sb=new StringBuilder("Name cannot be resolved; possible incorrect function/predicate call; " +
           "perhaps you used ( ) when you should have used [ ]\n");
        for(Expr x:choices) {
            pos = pos.merge(x.span());
            if (x instanceof ExprBadCall || x instanceof ExprBadJoin) sb.append('\n').append(x.errors.pick().msg);
        }
        return new ErrorType(pos, sb.toString());
    }

    //============================================================================================================//

    /** Constructs an ExprChoice node. */
    private ExprChoice(Pos pos, ConstList<Expr> choices, ConstList<String> reasons, Type type, long weight) {
        super(pos, null, true, type, 0, weight, emptyListOfErrors.make(type==EMPTY ? complain(pos,choices) : null));
        this.choices = choices;
        this.reasons = reasons;
    }

    //============================================================================================================//

    /** Construct an ExprChoice node. */
    public static Expr make(Pos pos, ConstList<Expr> choices, ConstList<String> reasons) {
        if (choices.size()==0) return new ExprBad(pos, "", new ErrorType(pos, "This expression failed to be typechecked."));
        if (choices.size()==1 && choices.get(0).errors.isEmpty()) return choices.get(0); // Shortcut
        Type type=EMPTY;
        boolean first=true;
        long weight=0;
        for(Expr x:choices) {
            type=x.type.merge(type);
            if (first || weight>x.weight) if (x.type!=EMPTY) { weight=x.weight; first=false; }
        }
        return new ExprChoice(pos, choices, reasons, type, weight);
    }

    //============================================================================================================//

    /** Resolve the list of choices, or return an ExprBad object containing the list of unresolvable ambiguities. */
    private Expr resolveHelper(boolean firstPass, final Type t, List<Expr> choices, List<String> reasons, Collection<ErrorWarning> warns) {
        List<Expr> ch = new ArrayList<Expr>(choices.size());
        List<String> re = new ArrayList<String>(choices.size());
        // We first prefer exact matches
        for(int i=0; i<choices.size(); i++) {
            Type tt = choices.get(i).type;
            if ((t.is_int && tt.is_int) || (t.is_bool && tt.is_bool) || t.intersects(tt)) { ch.add(choices.get(i)); re.add(reasons.get(i)); }
        }
        // If none, we try any legal matches
        if (ch.size()==0) {
            for(int i=0; i<choices.size(); i++) if (choices.get(i).type.hasCommonArity(t)) { ch.add(choices.get(i)); re.add(reasons.get(i)); }
        }
        // If none, we try sigint->int
        if (ch.size()==0 && Type.SIGINT2INT && t.is_int) {
            for(int i=0; i<choices.size(); i++) if (choices.get(i).type.intersects(SIGINT.type)) { ch.add(choices.get(i).cast2int()); re.add(reasons.get(i)); }
        }
        // If none, we try int->sigint
        if (ch.size()==0 && Type.INT2SIGINT && t.hasArity(1)) {
            for(int i=0; i<choices.size(); i++) if (choices.get(i).type.is_int) { ch.add(choices.get(i).cast2sigint()); re.add(reasons.get(i)); }
        }
        // If too many, then keep the choices with the smallest weight
        if (ch.size()>1) {
            List<Expr> ch2 = new ArrayList<Expr>(ch.size());
            List<String> re2 = new ArrayList<String>(ch.size());
            long w = 0;
            for(int i=0; i<ch.size(); i++) {
                Expr c = ch.get(i);
                String r = re.get(i);
                if (ch2.size()>0 && c.weight>w) continue; else if (ch2.size()==0 || c.weight<w) {ch2.clear(); re2.clear(); w=c.weight;}
                ch2.add(c);
                re2.add(r);
            }
            ch = ch2;
            re = re2;
            // If still too many, but this is the first pass, then try to resolve them all and try again
            if (firstPass && ch.size()>1) {
                ch2 = new ArrayList<Expr>(ch.size());
                for(Expr c:ch) ch2.add(c.resolve(t, null));
                return resolveHelper(false, t, ch2, re, warns);
            }
        }
        // If we are down to exactly 1 match, return it
        if (ch.size()==1) return ch.get(0).resolve(t, warns);
        // If we are faced with 2 or more choices, but they all result in emptyset-of-the-same-arity, then just return emptyset
        none:
        while(ch.size()>1) {
            int arity = -1;
            for(Expr c: ch) {
                if (c.type.is_bool || c.type.is_int || c.type.hasTuple()) break none;
                int a = c.type.arity();
                if (a<1) break none;
                if (arity<0) arity=a; else if (arity!=a) break none;
            }
            Expr ans = Sig.NONE;
            while(arity>1) {ans=ans.product(Sig.NONE); arity--;}
            return ExprUnary.Op.NOOP.make(span(), ans);
        }
        // Otherwise, complain!
        String txt;
        if (ch.size()>1) {
            txt="\nThis name is ambiguous due to multiple matches:";
        } else {
            txt="\nThis name cannot be resolved; its relevant type does not intersect with any of the following candidates:";
            re = reasons;
        }
        StringBuilder msg = new StringBuilder(txt);
        for(String r:re) msg.append('\n').append(r);
        return new ExprBad(pos, toString(), new ErrorType(pos, msg.toString()));
    }

    /** {@inheritDoc} */
    @Override public Expr resolve(Type t, Collection<ErrorWarning> warns) {
        if (errors.size()>0) return this; else return resolveHelper(true, t, choices, reasons, warns);
    }

    //============================================================================================================//

    /** {@inheritDoc} */
    public int getDepth() {
        int max = 1;
        for(Expr x: choices) { int tmp=x.getDepth(); if (max<tmp) max=tmp; }
        return 1 + max;
    }

    /** {@inheritDoc} */
    @Override final<T> T accept(VisitReturn<T> visitor) throws Err {
        if (!errors.isEmpty()) throw errors.pick();
        throw new ErrorType(span(), "This expression failed to be resolved.");
    }

    /** {@inheritDoc} */
    @Override public String getDescription() { return "<b>error</b> (parser or typechecker failed)"; }

    /** {@inheritDoc} */
    @Override public List<? extends Browsable> getSubnodes() { return new ArrayList<Browsable>(0); }
}
